Das Verfahren wird als vollautomatisch bezeichnet, weil es keiner Benutzerinteraktion bedarf (im Gegensatz zu einigen deduktiven Verfahren, wie zum Beispiel interaktives Theorembeweisen). Die Systembeschreibung erfolgt in einer formalen Sprache, zum Beispiel durch ein Programm, einen endlichen Automaten oder ein Transitionssystem. Der Zustandsraum...